Left Termination of the query pattern ackermann(b,b,f) w.r.t. the given Prolog program could successfully be proven:



PROLOG
  ↳ PrologToPiTRSProof

ackermann3(00, N, s1(N)).
ackermann3(s1(M), 00, Val) :- ackermann3(M, s1(00), Val).
ackermann3(s1(M), s1(N), Val) :- ackermann3(s1(M), N, Val1), ackermann3(M, Val1, Val).


With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


ackermann_3_in_gga3(0_0, N, s_11(N)) -> ackermann_3_out_gga3(0_0, N, s_11(N))
ackermann_3_in_gga3(s_11(M), 0_0, Val) -> if_ackermann_3_in_1_gga3(M, Val, ackermann_3_in_gga3(M, s_11(0_0), Val))
ackermann_3_in_gga3(s_11(M), s_11(N), Val) -> if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))
if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_in_gga3(M, Val1, Val))
if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_out_gga3(M, Val1, Val)) -> ackermann_3_out_gga3(s_11(M), s_11(N), Val)
if_ackermann_3_in_1_gga3(M, Val, ackermann_3_out_gga3(M, s_11(0_0), Val)) -> ackermann_3_out_gga3(s_11(M), 0_0, Val)

The argument filtering Pi contains the following mapping:
ackermann_3_in_gga3(x1, x2, x3)  =  ackermann_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ackermann_3_out_gga3(x1, x2, x3)  =  ackermann_3_out_gga1(x3)
if_ackermann_3_in_1_gga3(x1, x2, x3)  =  if_ackermann_3_in_1_gga1(x3)
if_ackermann_3_in_2_gga4(x1, x2, x3, x4)  =  if_ackermann_3_in_2_gga2(x1, x4)
if_ackermann_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ackermann_3_in_3_gga1(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_3_in_gga3(0_0, N, s_11(N)) -> ackermann_3_out_gga3(0_0, N, s_11(N))
ackermann_3_in_gga3(s_11(M), 0_0, Val) -> if_ackermann_3_in_1_gga3(M, Val, ackermann_3_in_gga3(M, s_11(0_0), Val))
ackermann_3_in_gga3(s_11(M), s_11(N), Val) -> if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))
if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_in_gga3(M, Val1, Val))
if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_out_gga3(M, Val1, Val)) -> ackermann_3_out_gga3(s_11(M), s_11(N), Val)
if_ackermann_3_in_1_gga3(M, Val, ackermann_3_out_gga3(M, s_11(0_0), Val)) -> ackermann_3_out_gga3(s_11(M), 0_0, Val)

The argument filtering Pi contains the following mapping:
ackermann_3_in_gga3(x1, x2, x3)  =  ackermann_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ackermann_3_out_gga3(x1, x2, x3)  =  ackermann_3_out_gga1(x3)
if_ackermann_3_in_1_gga3(x1, x2, x3)  =  if_ackermann_3_in_1_gga1(x3)
if_ackermann_3_in_2_gga4(x1, x2, x3, x4)  =  if_ackermann_3_in_2_gga2(x1, x4)
if_ackermann_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ackermann_3_in_3_gga1(x5)


Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_3_IN_GGA3(s_11(M), 0_0, Val) -> IF_ACKERMANN_3_IN_1_GGA3(M, Val, ackermann_3_in_gga3(M, s_11(0_0), Val))
ACKERMANN_3_IN_GGA3(s_11(M), 0_0, Val) -> ACKERMANN_3_IN_GGA3(M, s_11(0_0), Val)
ACKERMANN_3_IN_GGA3(s_11(M), s_11(N), Val) -> IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))
ACKERMANN_3_IN_GGA3(s_11(M), s_11(N), Val) -> ACKERMANN_3_IN_GGA3(s_11(M), N, Val1)
IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> IF_ACKERMANN_3_IN_3_GGA5(M, N, Val, Val1, ackermann_3_in_gga3(M, Val1, Val))
IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> ACKERMANN_3_IN_GGA3(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_3_in_gga3(0_0, N, s_11(N)) -> ackermann_3_out_gga3(0_0, N, s_11(N))
ackermann_3_in_gga3(s_11(M), 0_0, Val) -> if_ackermann_3_in_1_gga3(M, Val, ackermann_3_in_gga3(M, s_11(0_0), Val))
ackermann_3_in_gga3(s_11(M), s_11(N), Val) -> if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))
if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_in_gga3(M, Val1, Val))
if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_out_gga3(M, Val1, Val)) -> ackermann_3_out_gga3(s_11(M), s_11(N), Val)
if_ackermann_3_in_1_gga3(M, Val, ackermann_3_out_gga3(M, s_11(0_0), Val)) -> ackermann_3_out_gga3(s_11(M), 0_0, Val)

The argument filtering Pi contains the following mapping:
ackermann_3_in_gga3(x1, x2, x3)  =  ackermann_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ackermann_3_out_gga3(x1, x2, x3)  =  ackermann_3_out_gga1(x3)
if_ackermann_3_in_1_gga3(x1, x2, x3)  =  if_ackermann_3_in_1_gga1(x3)
if_ackermann_3_in_2_gga4(x1, x2, x3, x4)  =  if_ackermann_3_in_2_gga2(x1, x4)
if_ackermann_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ackermann_3_in_3_gga1(x5)
IF_ACKERMANN_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ACKERMANN_3_IN_2_GGA2(x1, x4)
IF_ACKERMANN_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_ACKERMANN_3_IN_3_GGA1(x5)
IF_ACKERMANN_3_IN_1_GGA3(x1, x2, x3)  =  IF_ACKERMANN_3_IN_1_GGA1(x3)
ACKERMANN_3_IN_GGA3(x1, x2, x3)  =  ACKERMANN_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_3_IN_GGA3(s_11(M), 0_0, Val) -> IF_ACKERMANN_3_IN_1_GGA3(M, Val, ackermann_3_in_gga3(M, s_11(0_0), Val))
ACKERMANN_3_IN_GGA3(s_11(M), 0_0, Val) -> ACKERMANN_3_IN_GGA3(M, s_11(0_0), Val)
ACKERMANN_3_IN_GGA3(s_11(M), s_11(N), Val) -> IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))
ACKERMANN_3_IN_GGA3(s_11(M), s_11(N), Val) -> ACKERMANN_3_IN_GGA3(s_11(M), N, Val1)
IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> IF_ACKERMANN_3_IN_3_GGA5(M, N, Val, Val1, ackermann_3_in_gga3(M, Val1, Val))
IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> ACKERMANN_3_IN_GGA3(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_3_in_gga3(0_0, N, s_11(N)) -> ackermann_3_out_gga3(0_0, N, s_11(N))
ackermann_3_in_gga3(s_11(M), 0_0, Val) -> if_ackermann_3_in_1_gga3(M, Val, ackermann_3_in_gga3(M, s_11(0_0), Val))
ackermann_3_in_gga3(s_11(M), s_11(N), Val) -> if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))
if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_in_gga3(M, Val1, Val))
if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_out_gga3(M, Val1, Val)) -> ackermann_3_out_gga3(s_11(M), s_11(N), Val)
if_ackermann_3_in_1_gga3(M, Val, ackermann_3_out_gga3(M, s_11(0_0), Val)) -> ackermann_3_out_gga3(s_11(M), 0_0, Val)

The argument filtering Pi contains the following mapping:
ackermann_3_in_gga3(x1, x2, x3)  =  ackermann_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ackermann_3_out_gga3(x1, x2, x3)  =  ackermann_3_out_gga1(x3)
if_ackermann_3_in_1_gga3(x1, x2, x3)  =  if_ackermann_3_in_1_gga1(x3)
if_ackermann_3_in_2_gga4(x1, x2, x3, x4)  =  if_ackermann_3_in_2_gga2(x1, x4)
if_ackermann_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ackermann_3_in_3_gga1(x5)
IF_ACKERMANN_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ACKERMANN_3_IN_2_GGA2(x1, x4)
IF_ACKERMANN_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_ACKERMANN_3_IN_3_GGA1(x5)
IF_ACKERMANN_3_IN_1_GGA3(x1, x2, x3)  =  IF_ACKERMANN_3_IN_1_GGA1(x3)
ACKERMANN_3_IN_GGA3(x1, x2, x3)  =  ACKERMANN_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 2 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
PiDP
              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_3_IN_GGA3(s_11(M), 0_0, Val) -> ACKERMANN_3_IN_GGA3(M, s_11(0_0), Val)
ACKERMANN_3_IN_GGA3(s_11(M), s_11(N), Val) -> ACKERMANN_3_IN_GGA3(s_11(M), N, Val1)
IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> ACKERMANN_3_IN_GGA3(M, Val1, Val)
ACKERMANN_3_IN_GGA3(s_11(M), s_11(N), Val) -> IF_ACKERMANN_3_IN_2_GGA4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))

The TRS R consists of the following rules:

ackermann_3_in_gga3(0_0, N, s_11(N)) -> ackermann_3_out_gga3(0_0, N, s_11(N))
ackermann_3_in_gga3(s_11(M), 0_0, Val) -> if_ackermann_3_in_1_gga3(M, Val, ackermann_3_in_gga3(M, s_11(0_0), Val))
ackermann_3_in_gga3(s_11(M), s_11(N), Val) -> if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_in_gga3(s_11(M), N, Val1))
if_ackermann_3_in_2_gga4(M, N, Val, ackermann_3_out_gga3(s_11(M), N, Val1)) -> if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_in_gga3(M, Val1, Val))
if_ackermann_3_in_3_gga5(M, N, Val, Val1, ackermann_3_out_gga3(M, Val1, Val)) -> ackermann_3_out_gga3(s_11(M), s_11(N), Val)
if_ackermann_3_in_1_gga3(M, Val, ackermann_3_out_gga3(M, s_11(0_0), Val)) -> ackermann_3_out_gga3(s_11(M), 0_0, Val)

The argument filtering Pi contains the following mapping:
ackermann_3_in_gga3(x1, x2, x3)  =  ackermann_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ackermann_3_out_gga3(x1, x2, x3)  =  ackermann_3_out_gga1(x3)
if_ackermann_3_in_1_gga3(x1, x2, x3)  =  if_ackermann_3_in_1_gga1(x3)
if_ackermann_3_in_2_gga4(x1, x2, x3, x4)  =  if_ackermann_3_in_2_gga2(x1, x4)
if_ackermann_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ackermann_3_in_3_gga1(x5)
IF_ACKERMANN_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ACKERMANN_3_IN_2_GGA2(x1, x4)
ACKERMANN_3_IN_GGA3(x1, x2, x3)  =  ACKERMANN_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
QDP
                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_3_IN_GGA2(s_11(M), 0_0) -> ACKERMANN_3_IN_GGA2(M, s_11(0_0))
ACKERMANN_3_IN_GGA2(s_11(M), s_11(N)) -> ACKERMANN_3_IN_GGA2(s_11(M), N)
IF_ACKERMANN_3_IN_2_GGA2(M, ackermann_3_out_gga1(Val1)) -> ACKERMANN_3_IN_GGA2(M, Val1)
ACKERMANN_3_IN_GGA2(s_11(M), s_11(N)) -> IF_ACKERMANN_3_IN_2_GGA2(M, ackermann_3_in_gga2(s_11(M), N))

The TRS R consists of the following rules:

ackermann_3_in_gga2(0_0, N) -> ackermann_3_out_gga1(s_11(N))
ackermann_3_in_gga2(s_11(M), 0_0) -> if_ackermann_3_in_1_gga1(ackermann_3_in_gga2(M, s_11(0_0)))
ackermann_3_in_gga2(s_11(M), s_11(N)) -> if_ackermann_3_in_2_gga2(M, ackermann_3_in_gga2(s_11(M), N))
if_ackermann_3_in_2_gga2(M, ackermann_3_out_gga1(Val1)) -> if_ackermann_3_in_3_gga1(ackermann_3_in_gga2(M, Val1))
if_ackermann_3_in_3_gga1(ackermann_3_out_gga1(Val)) -> ackermann_3_out_gga1(Val)
if_ackermann_3_in_1_gga1(ackermann_3_out_gga1(Val)) -> ackermann_3_out_gga1(Val)

The set Q consists of the following terms:

ackermann_3_in_gga2(x0, x1)
if_ackermann_3_in_2_gga2(x0, x1)
if_ackermann_3_in_3_gga1(x0)
if_ackermann_3_in_1_gga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ACKERMANN_3_IN_GGA2, IF_ACKERMANN_3_IN_2_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: